\begin{tabbing}
chain{-}replication\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it Config}$; ${\it Master}$; $u$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=master{-}constraints(${\it es}$;${\it Master}$)\+
\\[0ex]\& ($\exists$\=$c$:es{-}E{-}interface(${\it es}$;${\it Config}$)$\rightarrow$es{-}E{-}interface(${\it es}$;${\it Master}$)\+
\\[0ex]config{-}antecedent(${\it es}$;${\it Master}$;${\it Config}$;$c$))
\-\\[0ex]\& update{-}antecedent\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it Config}$; $u$)
\-\\[0ex]\& ($\exists$\=$m$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} $\rightarrow$es{-}E{-}interface(${\it es}$;${\it Config}$)\+
\\[0ex]master{-}antecedent\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Master}$; ${\it Config}$; ${\it Sys}$; $m$))
\-\-\\[0ex]\& es{-}interface{-}disjoint(${\it es}$;${\it Sys}$;${\it Config}$)
\-
\end{tabbing}